Nuprl Lemma : rv-partial-sum_wf 11,40

p:FinProbSpace, f:(), X:(n:RandomVariable(p;f(n))), n:.
(n:i:{0..n}. f(i) < f(n))  (rv-partial-sum(n;i.X(i))  RandomVariable(p;f(n))) 
latex


Definitionst  T, x:AB(x), Outcome, , {x:AB(x)} , x:AB(x), f(a), x(s), #$n, {i..j}, Type, FinProbSpace, a < b, A  B, x:A  B(x), P & Q, i  j < k, , Top, type List, P  Q, False, A, ||as||, Void, <ab>, s = t, True, T, S  T, suptype(ST), , , , A  B, x,y:A//B(x;y), if b then t else f fi , EquivRel(T;x,y.E(x;y)), tt, qeq(r;s), , x,yt(x;y), xt(x), a  j < bE(j), x.A(x), RandomVariable(p;n), rv-partial-sum(n;i.X(i))
Lemmasrandom-variable wf, finite-prob-space wf, qsum wf, int-rational, quotient wf, bool wf, qeq wf2, btrue wf, b-union wf, int nzero wf, rationals wf, subtype rel function, squash wf, true wf, int seg properties, length wf nat, le wf, int seg wf, nat wf, p-outcome wf

origin